\begin{tabbing}
ecl{-}es{-}act(${\it es}$;$m$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=ecl\_ind($x$;$k$,${\it test}$.$\lambda$$e_{1}$,$e_{2}$. False;$a$,$b$,${\it aa}$,${\it ab}$.$\lambda$$e_{1}$,$e_{2}$. ${\it aa}$($e_{1}$,$e_{2}$)\+
\\[0ex]$\vee$ \=existse{-}between3(${\it es}$;$e_{1}$;$e_{2}$;$e$.ecl{-}es{-}halt(${\it es}$;$a$)(0,$e_{1}$,es{-}pred(${\it es}$; $e$))\+
\\[0ex]\& ${\it ab}$($e$,$e_{2}$));$a$,$b$,${\it aa}$,${\it ab}$.$\lambda$$e_{1}$,$e_{2}$. ${\it aa}$($e_{1}$,$e_{2}$)
\-\\[0ex]\& $\forall$$n$$\in$ecl{-}ex($b$).alle{-}between1(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$ecl{-}es{-}halt(${\it es}$;$b$)($n$,$e_{1}$,$e$))
\\[0ex]$\vee$ \=${\it ab}$($e_{1}$,$e_{2}$)\+
\\[0ex]\& $\forall$\=$n$$\in$ecl{-}ex($a$).\+
\\[0ex]alle{-}between1(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$ecl{-}es{-}halt(${\it es}$;$a$)($n$,$e_{1}$,$e$));$a$,$b$,${\it aa}$,${\it ab}$.$\lambda$$e_{1}$,$e_{2}$. ${\it aa}$($e_{1}$,$e_{2}$)
\-\-\\[0ex]\& $\forall$$n$$\in$0.ecl{-}ex($b$).alle{-}between1(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$ecl{-}es{-}halt(${\it es}$;$b$)($n$,$e_{1}$,$e$))
\\[0ex]$\vee$ \=${\it ab}$($e_{1}$,$e_{2}$)\+
\\[0ex]\& $\forall$$n$$\in$0.ecl{-}ex($a$).alle{-}between1(${\it es}$;$e_{1}$;$e_{2}$;$e$.$\neg$ecl{-}es{-}halt(${\it es}$;$a$)($n$,$e_{1}$,$e$));$a$,${\it aa}$.$\lambda$$e_{1}$,$e_{2}$.
\-\\[0ex]es{-}pstar{-}q(${\it es}$;$x$,$y$.\=ecl{-}es{-}halt(${\it es}$;$a$)\+
\\[0ex](0
\\[0ex],$x$
\\[0ex],$y$);$x$,$y$.${\it aa}$($x$,$y$);$e_{1}$;$e_{2}$);$a$,$n$,${\it aa}$.\=if $m$=$_{2}$$n$$\rightarrow$ ecl{-}es{-}halt(${\it es}$;$a$)(0)\+
\\[0ex]else ${\it aa}$ fi;$a$,$n$,${\it aa}$.${\it aa}$;$a$,$l$,${\it aa}$.${\it aa}$)
\-\-\-
\end{tabbing}